\begin{tabbing}
event\_system\{i:l\}
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$E$:Type\+
\\[0ex]$\times$ (${\it eq}$:EqDecider($E$)
\\[0ex]$\times$ ${\it pred?}$:($E$$\rightarrow$(?$E$))
\\[0ex]$\times$ ${\it info}$:($E$$\rightarrow$((:Id $\times$ Id) + (:(:IdLnk $\times$ $E$) $\times$ Id)))
\\[0ex]$\times$ ${\it oaxioms}$:EOrderAxioms($E$;${\it pred?}$;${\it info}$)
\\[0ex]$\times$ $T$:(Id$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$ $V$:(Id$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$ $M$:(IdLnk$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$ ${\it init}$:($i$:Id$\rightarrow$EState(($T$($i$))))
\\[0ex]$\times$ ${\it Trans}$:\=($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.($V$($i$,$a$)); $l$,$t$.($M$($l$,$t$)))$\rightarrow$EState(($T$($i$)))$\rightarrow$EState\+
\\[0ex](($T$($i$))))
\-\\[0ex]$\times$ ${\it val}$:($e$:$E$$\rightarrow$kindcase(kind($e$); $a$.($V$(loc($e$),$a$)); $l$,$t$.($M$($l$,$t$))))
\\[0ex]$\times$ ${\it Send}$:\=($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.($V$($i$,$a$)); $l$,$t$.($M$($l$,$t$)))$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$\+
\\[0ex](Msg($M$) List))
\-\\[0ex]$\times$ ${\it Choose}$:($i$,$a$:Id$\rightarrow\mathbb{N}\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$(?($V$($i$,$a$))))
\\[0ex]$\times$ ${\it time}$:($E$$\rightarrow$rationals)
\\[0ex]$\times$ ${\it va}$:\=val{-}axiom($E$;$V$;$M$;${\it info}$;${\it pred?}$;\+
\\[0ex]${\it init}$;${\it Trans}$;
\\[0ex]${\it Choose}$;${\it Send}$;${\it val}$;${\it time}$)
\-\\[0ex]$\times$ ${\it opres}$:($\forall$$e$,${\it e'}$:$E$. $e$ $<$ ${\it e'}$ $\Rightarrow$ qle((${\it time}$($e$)); (${\it time}$(${\it e'}$))))
\\[0ex]$\times$ ${\it discrete}$:(Id$\rightarrow$Id$\rightarrow\mathbb{B}$)
\\[0ex]$\times$ (${\it consts}$:\=($\forall$$i$,$x$:Id.\+
\\[0ex]($\uparrow$(${\it discrete}$($i$,$x$)))
\\[0ex]$\Rightarrow$ \=(constant\_function((${\it init}$($i$,$x$)); rationals; ($T$($i$,$x$)))\+
\\[0ex]$\wedge$ \=($\forall$$k$:Knd, $v$:kindcase($k$; $a$.($V$($i$,$a$)); $l$,$t$.($M$($l$,$t$))), $s$:EState(($T$($i$))).\+
\\[0ex]constant\_function(($s$($x$)); rationals; ($T$($i$,$x$)))
\\[0ex]$\Rightarrow$ constant\_function((${\it Trans}$($i$,$k$,$v$,$s$,$x$)); rationals; ($T$($i$,$x$))))))
\-\-\-\\[0ex]$\times$ top))
\-
\end{tabbing}